g:GrpSig, s:(|g|). norm_subset_p(g;s)   

latex

Up	groups 1
Definitions of Statement	norm_subset_p(g;s)
Definitions	x f y, P  Q, norm_subset_p(g;s), t  T, , x:A. B(x)
Lemmas	grp sig wf, grp inv wf, grp op wf, grp car wf